package bcontractor.partialmeet.operator;

import bcontractor.api.SATReasoner;
import bcontractor.api.Sentence;
import bcontractor.builder.Builder;
import bcontractor.builders.BuilderHelper;
import bcontractor.builders.NullBuilder;
import bcontractor.partialmeet.operators.BlackboxRemainderSetOperator;
import bcontractor.propositional.MiniSatReasonerBuilder;
import bcontractor.propositional.PropositionalSentence;

/**
 * Builder for BlackboxRemainderSetOperator
 * 
 * @author lundberg
 * 
 */
public class BlackboxRemainderSetOperatorBuilder<S extends Sentence<S>> implements Builder<BlackboxRemainderSetOperator<S>> {

    private Builder<SATReasoner<S>> reasoner = new NullBuilder<SATReasoner<S>>();

    /**
     * 
     * @return BlackboxKernelResolverBuilder
     */
    public static BlackboxRemainderSetOperatorBuilder<PropositionalSentence> aRemainderSetOperator() {
        return new BlackboxRemainderSetOperatorBuilder<PropositionalSentence>().having(new MiniSatReasonerBuilder());
    }

    /**
     * {@inheritDoc}
     */
    @Override
    public BlackboxRemainderSetOperator<S> build() {
        return new BlackboxRemainderSetOperator<S>(this.reasoner.build());
    }

    /**
     * @param reasoner
     */
    public BlackboxRemainderSetOperatorBuilder<S> having(Builder<? extends SATReasoner<S>> reasoner) {
        return BuilderHelper.copyWith(this, "reasoner", reasoner);
    }
}
